package typesys;

import java.util.ArrayList;

import flowlogic.STSimplifier;

import ast.AtomicLabel;
import ast.Label;
import ast.LabelConjunction;
import ast.LabelDisjunction;
import ast.Principal;
import ast.Term;
import ast.TermVar;

public class RelabellingJudgement extends TypeJudgement {
	
	private Label l1;
	private Label l2;
	
	public RelabellingJudgement(PrincipalHierarchy ph, Label l1, Label l2) 
	{
		setHierarchy(ph);
		// the externality information is not used for relabelling
		this.l1 = flattenLabel(STSimplifier.simplifyLabel(l1));
		this.l2 = flattenLabel(STSimplifier.simplifyLabel(l2));
	}

	public boolean check()
	{
		boolean result = false;
		
		RelabellingJudgement rejgt;
		
		if (l1 instanceof AtomicLabel && l2 instanceof AtomicLabel) {
			
			result = true;
			
			AtomicLabel al1 = (AtomicLabel) l1;
			AtomicLabel al2 = (AtomicLabel) l2;
			Term o1 = ((AtomicLabel) l1).getOwner();
			Term o2 = ((AtomicLabel) l2).getOwner();
			PrincipalHierarchy ph = getHierarchy();
			
			if (!ph.actsFor(getPrFromT(o1), getPrFromT(o2))) {
				result = false;
			} else {
				for (Term t : al1.getInfluencers()) {
					Principal influencer1 = getPrFromT(t);
					if (!ph.actsFor(influencer1, getPrFromT(o2))) {
						boolean innerResult = false;
						for (Term t2 : al2.getInfluencers()) {
							if (ph.actsFor(influencer1, getPrFromT(t2))) {
								innerResult = true;
								break;
							}
						}
						if (!innerResult) {
							result = false;
							break;
						}
					}
				}
			}
			
		} else if ((l1 instanceof LabelConjunction || l1 instanceof AtomicLabel) && 
				   (l2 instanceof LabelConjunction || l2 instanceof AtomicLabel)) {
			
			result = true;
			
			ArrayList<Label> list1;
			ArrayList<Label> list2;
			if (l1 instanceof AtomicLabel) {
				list1 = new ArrayList<Label>();
				list1.add(l1);
			} else {
				list1 = ((LabelConjunction) l1).getOps(); 
			}
			if (l2 instanceof AtomicLabel) {
				list2 = new ArrayList<Label>();
				list2.add(l2);
			} else {
				list2 = ((LabelConjunction) l2).getOps();
			}
			
			for (Label lbRight : list2) {
				boolean innerResult = false;
				for (Label lbLeft : list1) {
					rejgt = new RelabellingJudgement(getHierarchy(), lbLeft, lbRight);
					if (rejgt.check()) {
						innerResult = true;
						break;
					}
				}
				if (!innerResult) {
					result = false;
					break;
				}
			}
			
		} else if ((l1 instanceof LabelDisjunction || l1 instanceof AtomicLabel) && 
				   (l2 instanceof LabelDisjunction || l2 instanceof AtomicLabel)) {
			
			ArrayList<Label> list1;
			ArrayList<Label> list2;
			if (l1 instanceof AtomicLabel) {
				list1 = new ArrayList<Label>();
				list1.add(l1);
			} else {
				list1 = ((LabelDisjunction) l1).getOps(); 
			}
			if (l2 instanceof AtomicLabel) {
				list2 = new ArrayList<Label>();
				list2.add(l2);
			} else {
				list2 = ((LabelDisjunction) l2).getOps();
			}
			
			result = true;
			for (Label lbLeft : list1) {
				boolean innerResult = false;
				for (Label lbRight : list2) {
					rejgt = new RelabellingJudgement(getHierarchy(), lbLeft, lbRight);
					if (rejgt.check()) {
						innerResult = true;
						break;
					}
				}
				if (!innerResult) {
					result = false;
					break;
				}
			}
			
		} else {
			
			if (l1 instanceof LabelConjunction) {
				
				result = false;
				for (Label lb : ((LabelConjunction) l1).getOps()) {
					rejgt = new RelabellingJudgement(getHierarchy(), lb, l2);
					if (rejgt.check()) {
						result = true;
						break;
					}
				}
				
			} else if (l1 instanceof LabelDisjunction) {
				
				result = true;
				for (Label lb : ((LabelDisjunction) l1).getOps()) {
					rejgt = new RelabellingJudgement(getHierarchy(), lb, l2);
					if (!rejgt.check()) {
						result = false;
						break;
					}
				}
				
			} else {
				assert false;
			}
			
		}
		
		return result;
	}
	
	private Principal getPrFromT(Term t)
	{
		Principal result = null;
		
		if (t instanceof TermVar) {
			if (STSimplifier.getPrincipals().contains(((TermVar) t).getName())) 
				result =  new Principal(((TermVar) t).getName());
			else if (((TermVar) t).getName().equals("*")) 
				result = TopPrincipal.getInstance();
			else if (((TermVar) t).getName().equals("_"))
				result = BottomPrincipal.getInstance();
		} else if (t instanceof Principal) {
			result = (Principal) t;
		}
		
		return result;
	}
	
	private Label flattenLabel(Label label)
	{
		Label result = null;
		
		if (label instanceof LabelConjunction) {
			
			boolean allCon = true;
			for (Label op : ((LabelConjunction) label).getOps()) {
				if (! (op instanceof LabelConjunction)) {
					allCon = false;
					break;
				}
			}
			if (allCon) {
				ArrayList<Label> components = new ArrayList<Label>();
				for (Label op : ((LabelConjunction) label).getOps()) {
					for (Label opInner : ((LabelConjunction) op).getOps()) {
						components.add(flattenLabel(opInner));
					}
				}
				result = new LabelConjunction(components);
			} else {
				result = label;
			}
			
		} else if (label instanceof LabelDisjunction) {
			
			boolean allDis = true;
			for (Label op : ((LabelDisjunction) label).getOps()) {
				if (! (op instanceof LabelDisjunction)) {
					allDis = false;
					break;
				}
			}
			if (allDis) {
				ArrayList<Label> components = new ArrayList<Label>();
				for (Label op: ((LabelDisjunction) label).getOps()) {
					for (Label opInner : ((LabelDisjunction) op).getOps()) {
						components.add(flattenLabel(opInner));
					}
				}
				result = new LabelDisjunction(components);
			} else {
				result = label;
			}
		} else if (label instanceof AtomicLabel) {
			result = label;
		}
		
		return result;
	}
	
}
